the_w:World, l:IdLnk, mss:Msg List. onlnk(l;mss)  {m:Msg| mlnk(m) = l } List 

latex

Definitions	t  T, World, IdLnk, x:A. B(x), onlnk(l;mss), s = t, <a,b>, x:AB(x), S  T, mlnk(m), a = b, b, Msg, {x:A| B(x) }, type List, x:AB(x), Msg(M), Type, x.A(x), 1of(t), P  Q, P & Q, P  Q
Lemmas	assert-eq-lnk, subtype rel list, filter type, assert wf, eq lnk wf, w-onlnk wf, w-Msg wf, IdLnk wf, world wf